r:CRng, p:Ideal(r){i}, d:detach_fun(|r|;p).
(u:|r|. SqStable(p(u)))  (IsPrimeIdeal(r;p)  IsIntegDom(r / d)) 

latex

Up	rings 1
Definitions of Statement	0, *, 1, Rng, CRng, Ideal(r){i}, r / d, IsPrimeIdeal(R;P)
Definitions	, t  T, P  Q, x:A. B(x), P  Q, x f y, P & Q, P  Q, P  Q, a  b  T , x. t(x), t.2, t.1, [x]{T}, *, 0, 1, r / d, True, T, Rng, Ideal(r){i}, CRng, {T}, x(s), IsPrimeIdeal(R;P)
Lemmas	crng wf, ideal wf, detach fun wf, sq stable wf, rng car wf, idom alt char, rng times wf, rng one wf, rng zero wf, nequal wf, quot ring wf, integ dom p wf, prime ideal p wf, iff functionality wrt iff, equal symmetry, not functionality wrt iff, and functionality wrt iff, not wf, or functionality wrt iff, implies functionality wrt iff, quot ring car elim b, all functionality wrt iff, decidable rng eq, decidable or, sq stable from decidable, sq stable all, all rng quot elim a, rng minus wf, rng plus wf, type inj wf for qrng, iff wf, iff transitivity, rng plus zero, rng plus comm, rng minus zero, true wf, squash wf